Nuprl Definition : conditional
11,40
postcript
pdf
[
P
?
f
:
g
](
x
) == if
p
:
P
(
x
) then
f
(
x
) else
g
(
x
) fi
latex
clarification:
conditional(
P
;
dcd_P
;
f
;
g
)(
x
) == branch(
P
(
x
);
dcd_P
(
x
);
p
.
f
(
x
);
g
(
x
))
latex
Definitions
x
.
A
(
x
)
,
if
p
:
P
then
A
(
p
) else
B
fi
,
f
(
a
)
FDL editor aliases
conditional
origin
x.A(x)x.A(x)